PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 11:35:53 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -e 5e-2 -heuristic speed -ddextraactionvars 100 -maxiters 1000000 crowds.prism crowds.props --property positive -const 'TotalRuns=5,CrowdSize=20'
Parsing model file "crowds.prism"...
Type: DTMC
Modules: crowds
Variables: launch new runCount start run lastSeen good bad recordLast badObserve deliver done observe0 observe1 observe2 observe3 observe4 observe5 observe6 observe7 observe8 observe9 observe10 observe11 observe12 observe13 observe14 observe15 observe16 observe17 observe18 observe19
Parsing properties file "crowds.props"...
1 property:
(1) "positive": P=? [ F observe0>1 ]
---------------------------------------------------------------------
Model checking: "positive": P=? [ F observe0>1 ]
Model constants: TotalRuns=5,CrowdSize=20
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Model constants: TotalRuns=5,CrowdSize=20
Warning: Guard for command 6 of module "crowds" is never satisfied.
Warning: Guard for command 7 of module "crowds" is never satisfied.
Warning: Guard for command 8 of module "crowds" is never satisfied.
Warning: Guard for command 9 of module "crowds" is never satisfied.
Warning: Guard for command 10 of module "crowds" is never satisfied.
Warning: Guard for command 2 of module "crowds" overlaps with previous commands.
Warning: Guard for command 3 of module "crowds" overlaps with previous commands.
Warning: Guard for command 4 of module "crowds" overlaps with previous commands.
Warning: Guard for command 5 of module "crowds" overlaps with previous commands.
Warning: Guard for command 11 of module "crowds" overlaps with previous commands.
Warning: Guard for command 12 of module "crowds" overlaps with previous commands.
Warning: Guard for command 13 of module "crowds" overlaps with previous commands.
Warning: Guard for command 14 of module "crowds" overlaps with previous commands.
Warning: Guard for command 15 of module "crowds" overlaps with previous commands.
Warning: Guard for command 16 of module "crowds" overlaps with previous commands.
Warning: Guard for command 17 of module "crowds" overlaps with previous commands.
Warning: Guard for command 18 of module "crowds" overlaps with previous commands.
Warning: Guard for command 19 of module "crowds" overlaps with previous commands.
Warning: Guard for command 20 of module "crowds" overlaps with previous commands.
Warning: Guard for command 21 of module "crowds" overlaps with previous commands.
Warning: Guard for command 22 of module "crowds" overlaps with previous commands.
Warning: Guard for command 23 of module "crowds" overlaps with previous commands.
Warning: Guard for command 24 of module "crowds" overlaps with previous commands.
Warning: Guard for command 25 of module "crowds" overlaps with previous commands.
Warning: Guard for command 26 of module "crowds" overlaps with previous commands.
Warning: Guard for command 27 of module "crowds" overlaps with previous commands.
Warning: Guard for command 28 of module "crowds" overlaps with previous commands.
Warning: Guard for command 29 of module "crowds" overlaps with previous commands.
Warning: Guard for command 30 of module "crowds" overlaps with previous commands.
Warning: Guard for command 31 of module "crowds" overlaps with previous commands.
Warning: Guard for command 32 of module "crowds" overlaps with previous commands.
Warning: Guard for command 33 of module "crowds" overlaps with previous commands.
Computing reachable states...
Reachability (BFS): 47 iterations in 0.40 seconds (average 0.008596, setup 0.00)
Time for model construction: 0.422 seconds.
Warning: Deadlocks detected and fixed in 53130 states
Type: DTMC
States: 2061951 (1 initial)
Transitions: 7374951
Transition matrix: 33232 nodes (7 terminal), 7374951 minterms, vars: 78r/78c
Prob0: 14 iterations in 0.13 seconds (average 0.009143, setup 0.00)
Prob1: 30 iterations in 0.12 seconds (average 0.004100, setup 0.00)
yes = 47399, no = 1745849, maybe = 268703
Computing remaining probabilities...
Engine: Sparse
Building sparse matrix... [n=2061951, nnz=1756343, compact] [8.7 MB]
Creating vector for diagonals... [dist=1, compact] [3.9 MB]
Creating vector for RHS... [dist=2, compact] [3.9 MB]
Allocating iteration vectors... [ 2 x 15.7 MB]
TOTAL: [48.0 MB]
Starting iterations...
Max relative diff between upper and lower bound on convergence: 0.0439702
Backwards Gauss-Seidel (interval iteration): 87 iterations in 6.28 seconds (average 0.037506, setup 3.02)
Value in the initial state: 0.08794037364222435
Time for model checking: 6.537 seconds.
Result: 0.08794037364222435 (value in the initial state)
Overall running time: 7.541 seconds.
---------------------------------------------------------------------
Note: There were 34 warnings during computation.